$\forall$$R$:Realizer, $i$:Id. R{-}state($R$;$i$) $\in$ $x$:Id fp$\rightarrow$ Type